﻿//
// MainPage.xaml.cpp
// Implementation of the MainPage class.
//

#include "pch.h"
#include "MainPage.xaml.h"

using namespace OverSatX;

using namespace concurrency;
using namespace Platform;
using namespace Windows::Storage;
using namespace Windows::Storage::Pickers;
using namespace Windows::Storage::Streams;
using namespace Windows::Foundation;
using namespace Windows::Foundation::Collections;
using namespace Windows::System::Threading;
using namespace Windows::UI::Xaml;
using namespace Windows::UI::Xaml::Controls;
using namespace Windows::UI::Xaml::Controls::Primitives;
using namespace Windows::UI::Xaml::Data;
using namespace Windows::UI::Xaml::Input;
using namespace Windows::UI::Xaml::Media;
using namespace Windows::UI::Xaml::Navigation;

// The Blank Page item template is documented at http://go.microsoft.com/fwlink/?LinkId=402352&clcid=0x409

MainPage::MainPage() : sat_solver( nullptr )
{
	InitializeComponent();
	SetStatus(L"Ready");
	tbRootConflicts->Visibility = Windows::UI::Xaml::Visibility::Collapsed;
	spRootConflicts->Visibility = Windows::UI::Xaml::Visibility::Collapsed;
	std::list<std::string> self_test_results;
	solver::decision_string_collection dsc;
	dsc.self_test(self_test_results);

}

void OverSatX::MainPage::btnCnfLoad_Click(Platform::Object^ sender, Windows::UI::Xaml::RoutedEventArgs^ e)
{
	FileOpenPicker^ openPicker = ref new FileOpenPicker();
	openPicker->ViewMode = PickerViewMode::List;
	openPicker->SuggestedStartLocation = PickerLocationId::DocumentsLibrary;
	openPicker->FileTypeFilter->Append(".cnf");

	auto dataReader = std::make_shared<DataReader^>(nullptr);

	SetStatus(L"LOADING");

	create_task(openPicker->PickSingleFileAsync())
		.then([this](StorageFile^ file) 
	{
		tbRootConflicts->Visibility = Windows::UI::Xaml::Visibility::Collapsed;
		spRootConflicts->Visibility = Windows::UI::Xaml::Visibility::Collapsed;
		if (file)
		{
			SetStatus(L"FOUND");
			return file->OpenAsync(FileAccessMode::Read);
		}
		else
		{
			SetStatus(L"CANCELLED");
			throw task_canceled();
		}
	})
	.then([this,dataReader](IRandomAccessStream^ stream)-> IAsyncOperation<unsigned int>^
	{
		SetStatus(L"READING");
		*dataReader = ref new DataReader(stream->GetInputStreamAt(0));
		return (*dataReader)->LoadAsync(stream->Size);
	})
	.then([this, dataReader](unsigned int nbytes)
	{
		SetStatus(L"READ");
		textFileContent = (*dataReader)->ReadString(nbytes);
		solver::file_data fd(textFileContent);
		SetStatus(L"PARSE");
		sat_solver = sat_solver_factory.create_problem(fd);
		spDecisionString->Children->Clear();
		spRootConflicts->Children->Clear();
		DrawProblem();
		this->btnSATStep->IsEnabled = true;
		this->btnSATCalc->IsEnabled = true;
		this->btnSATStop->IsEnabled = false;
		SetStatus(L"LOADED");

	});
}

void MainPage::DrawEverything(bool finished)
{
	bool failures = false;
	sat::sat_solver_strategy strategy;

	spDecisionString->Children->Clear();
	spRootConflicts->Children->Clear();
	strategy.draw_decision_string(spDecisionString, sat_solver, sat_solver->solution);

	if (finished)
	{
		if (sat_solver->solved)
		{
			SetStatus(L"SOLVED");
			tbRootConflicts->Visibility = Windows::UI::Xaml::Visibility::Collapsed;
			spRootConflicts->Visibility = Windows::UI::Xaml::Visibility::Collapsed;
		}
		else
		{
			SetStatus(L"NOT SOLVED");
			tbRootConflicts->Visibility = Windows::UI::Xaml::Visibility::Collapsed;
			spRootConflicts->Visibility = Windows::UI::Xaml::Visibility::Collapsed;

			failures = true;
/*
			for (auto& fail : sat_solver->unsolvable)
			{
				strategy.draw_decision_string(spAllSimplifiedConflicts, sat_solver, *fail);
			}
			*/
		}
		this->btnSATStep->IsEnabled = false;
		this->btnSATCalc->IsEnabled = false;
		this->btnSATStop->IsEnabled = false;
		this->btnCnfLoad->IsEnabled = true;
	}
	else 
	{
		SetStatus(L"CONFLICT");
		tbRootConflicts->Visibility = Windows::UI::Xaml::Visibility::Visible;
		spRootConflicts->Visibility = Windows::UI::Xaml::Visibility::Visible;
	}

	if (!failures)
	{
		bool connector = false;
		Windows::UI::Xaml::Controls::TextBlock^ tbTextBlock = ref new Windows::UI::Xaml::Controls::TextBlock();
		std::wstring text;
/*		text = std::to_wstring(sat_solver->conflicts.get_count());
		text += L"  conflicts";
		Platform::String^ str = ref new Platform::String(text.c_str());
		tbTextBlock->Text = str;
		spAllSimplifiedConflicts->Children->Append(tbTextBlock);
		*/
		/*
		connector = false;
		int k = 0;
		for (auto& dec : sat_solver->conflicts)
		{
			if (++k > 100)
				break;
			strategy.draw_decision_string(spAllSimplifiedConflicts, sat_solver, *dec);
			connector = true;
		}*/
	}

	DrawProblem();

}

bool MainPage::SingleStep(  )
{
	sat::sat_solver_strategy strategy;
	bool finished = false;
	if (sat_solver)
	{
		finished = sat_solver->step(strategy);
		DrawEverything(finished);
	}

	return finished;
}

void OverSatX::MainPage::btnSATStep_Click(Platform::Object^ sender, Windows::UI::Xaml::RoutedEventArgs^ e)
{
	SingleStep();
}

void OverSatX::MainPage::RunBackground()
{
	IsRunning = true;
	IsStopped = false;
	btnSATStep->IsEnabled = false;
	btnSATCalc->IsEnabled = false;
	btnCnfLoad->IsEnabled = false;
	btnSATStop->IsEnabled = true;
	SetStatus(L"RUNNING");

	ThreadPool::RunAsync(ref new WorkItemHandler([this](IAsyncAction ^async)
	{
		Windows::Globalization::Calendar^ currentTime = ref new Windows::Globalization::Calendar();
		Windows::Globalization::Calendar^ endTime = ref new Windows::Globalization::Calendar();
		endTime->SetToNow();
		endTime->AddSeconds(1);
		Windows::Foundation::DateTime endDateTime = endTime->GetDateTime();

		sat::sat_solver_strategy strategy;
		bool finished = false;
		while (!finished && IsRunning)
		{
			if (sat_solver)
			{
				finished = sat_solver->step(strategy);
				currentTime->SetToNow();
				if (currentTime->CompareDateTime(endDateTime) > 0 || finished)
				{
					IsRunning = false;
					IsStopped = true;
					Windows::ApplicationModel::Core::CoreApplication::MainView->CoreWindow->Dispatcher->RunAsync(
						Windows::UI::Core::CoreDispatcherPriority::High,
						ref new Windows::UI::Core::DispatchedHandler([this, finished]()
					{
						DrawEverything(finished);
						if (!finished) 
						{
							RunBackground();
						}
					}));
					return;
				}
			}
		}

		if (!finished)
		{
			Windows::ApplicationModel::Core::CoreApplication::MainView->CoreWindow->Dispatcher->RunAsync(
				Windows::UI::Core::CoreDispatcherPriority::High,
				ref new Windows::UI::Core::DispatchedHandler([this, finished]()
			{
				// nasty side effects driven business... but that's why this app is a learning experience.
				btnSATStep->IsEnabled = true;
				btnSATCalc->IsEnabled = true;
				btnCnfLoad->IsEnabled = true;
				btnSATStop->IsEnabled = false;
				SetStatus(L"STOPPED");
			}));
		}

		IsStopped = true;
	}));
}

void OverSatX::MainPage::btnSATCalc_Click(Platform::Object^ sender, Windows::UI::Xaml::RoutedEventArgs^ e)
{
	if (IsRunning || !IsStopped)
		return;

	RunBackground();
}

void OverSatX::MainPage::btnSATStop_Click(Platform::Object^ sender, Windows::UI::Xaml::RoutedEventArgs^ e)
{
	IsRunning = false;
}

void MainPage::DrawProblem()
{
	solver::decision *lastdec = nullptr;
	sat::sat_solver_strategy strategy;
	spSATExpression->Children->Clear();
	int ds = sat_solver->decisions.size();
	if (ds > 0)
	{
		lastdec = sat_solver->decisions[ds - 1];
	}
	for (int i = 0; i < ds; i++)
	{
		auto dec = sat_solver->decisions[i];
		strategy.draw_decision(spSATExpression, sat_solver, *dec, dec != lastdec);
	}
	
	spConflictLanguage->Children->Clear();
	int cls = sat_solver->productions.size();
	for (int i = 0; i < ds; i++)
	{
		auto prod = sat_solver->productions[i];	
		if (prod) {
			strategy.draw_production(spConflictLanguage, sat_solver, prod);
		}
	}

}

void OverSatX::MainPage::SetStatus(const wchar_t *statusText)
{
	Platform::String^ strStatusText = ref new Platform::String(statusText);
	tbStatus->Text = strStatusText;
	if (sat_solver != nullptr) 
	{
		std::wstring passes = std::to_wstring(sat_solver->pass_count);
		strStatusText = ref new Platform::String(passes.c_str());
		tbPasses->Text = strStatusText;
	}
	else 
	{
		strStatusText = ref new Platform::String(L"N/A");
		tbPasses->Text = strStatusText;
	}
}
